(set-logic QF_UF)
(declare-sort u1 0)
(declare-sort u2 0)
(declare-fun Concat (Bool u1) u2)
(declare-fun y () Bool)
(declare-fun mod () Bool)
(declare-fun n1 () u1)
(declare-fun n2 () u2)
(declare-fun w2 () u2)
(declare-fun w5 () u2)

(assert (= w5 (Concat false n1)))
(assert (= n2 w5))
(assert (= w2 (Concat mod n1)))
(assert (= mod (not y)))
(assert (not (= n2 w2)))
(check-sat)
(exit)
